a:Id, T:Type, ds:x:Id fp Type, P:Top, init:x:Id fp ds(x)?Void, a1:Id, T1:Type, d1:x:Id fp Type,
P1:Top, i1:x:Id fp d1(x)?Void.
ds || d1
 init || i1
 a = a1
 (with ds: ds init: initaction a:T precondition a(v) is P
 (||+ with ds: d1 init: i1action a1:T1 precondition a1(v) is P1) 

latex

Definitions

x:A. B(x), P  Q, f || g, A ||+ B, with ds: ds init: initaction a:T precondition a(v) is P, P & Q, M1 || M2, ma-frame-compatible(A;B), mk-ma, x : v, , M1 ||decl M2, 1of(t), 2of(t), Prop, b, x  dom(f), f(x), deq-member(eq;x;L), reduce(f;k;as), false, Y, if b t else f fi, t  T, P  Q, P  Q, ma-frame-compat(A;B), xdom(f). v=f(x)   P(x;v), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), z != f(x)  P(a;z), x. t(x), a:A fp B(a), A, False, P  Q, x(s)

Lemmas

assert wf, deq-member wf, assert of bor, deq property, locl one one, or functionality wrt iff, false wf, not wf, Id wf, fpf-compatible wf, fpf-cap wf, fpf-join wf, id-deq wf, subtype-fpf3, strong-subtype-self, subtype-fpf-cap-void, fpf-sub-join-left, fpf-sub-join-right, fpf wf, top wf